es:event_system{i:l}, i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type).
es-decls(es;i;ds;da)  prop{i:l} 

latex

Definitions	Id, Knd, es-decls(es;i;ds;da), l-all(L; x.P(x)), event_system{i:l}, (x  l), fpf-domain(f), es-vartype(es; i; x), let x = a in b(x), fpf-ap(f; eq; x), es-E(es), P  Q, loc(e), es-isrcv(es; e), prop{i:l}, es-kind(es; e), es-valtype(es; e), b, id-deq, P  Q, P  Q, P  Q, P  Q, fpf(A; a.B(a)), top, x. t(x), x:A. B(x), Kind-deq, t  T
Lemmas	Kind-deq wf, Knd wf, fpf-trivial-subtype-top, member-fpf-domain, id-deq wf, Id wf, es-valtype wf, subtype rel wf, es-kind wf, es-isrcv wf, assert wf, es-loc wf, es-E wf, fpf-ap wf, let wf, es-vartype wf, fpf-domain wf, l member wf, l-all wf, event system wf, fpf wf